Java Modeling Language
part 2/4 · 12.1 KB total
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
Syntax
JML specifications are added to Java code in the form of annotations in
comments. Java comments are interpreted as JML annotations when they
begin with an @ sign. That is, comments of the form
//@ <JML specification>
or
/*@ <JML specification> @*/
Basic JML syntax provides the following keywords
requires
Defines a precondition on the method that follows.
ensures
Defines a postcondition on the method that follows.
signals
Defines a postcondition for when a given Exception is thrown by the
method that follows.
signals_only
Defines what exceptions may be thrown when the given precondition
holds.
assignable
Defines which fields are allowed to be assigned to by the method that
follows.
pure
Declares a method to be side effect free (like assignable \nothing
but can also throw exceptions). Furthermore, a pure method is supposed
to always either terminate normally or throw an exception.
invariant
Defines an invariant property of the class.
loop_invariant
Defines a loop invariant for a loop.
also
Combines specification cases and can also declare that a method is
inheriting specifications from its supertypes.
assert
Defines a JML assertion.
spec_public
Declares a protected or private variable public for specification
purposes.
Basic JML also provides the following expressions
\result
An identifier for the return value of the method that follows.
\old(<expression>)
A modifier to refer to the value of the <expression> at the time of
entry into a method.
(\forall <decl>; <range-exp>; <body-exp>)
The universal quantifier.
(\exists <decl>; <range-exp>; <body-exp>)
a ==> b
a implies b
a <== b
a is implied by b
a <==> b
a if and only if b
as well as standard Java syntax for logical and, or, and not. JML
annotations also have access to Java objects, object methods and
operators that are within the scope of the method being annotated and
that have appropriate visibility. These are combined to provide formal
specifications of the properties of classes, fields and methods. For
example, an annotated example of a simple banking class may look like
public class BankingExample
{
public static final int MAX_BALANCE = 1000;
private /*@ spec_public @*/ int balance;
private /*@ spec_public @*/ boolean isLocked = false;
//@ public invariant balance >= 0 && balance <= MAX_BALANCE;
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────